i:Id, ds1,ds2:fpf(Id; x.Type), da:fpf(Knd; k.Type), x,y:Id, T1,T2:Type, ks1,ks2:(Knd List),
tr1:(k:{k:Knd| (k  ks1)} decl-state(ds1)ma-valtype(da; k)T1T1),
tr2:(k:{k:Knd| (k  ks2)} decl-state(ds2)ma-valtype(da; k)T2T2).
((x = y))
 fpf-compatible(Id; a.Type; id-deq; ds1; fpf-single(x; T1))
 fpf-compatible(Id; a.Type; id-deq; ds2; fpf-single(y; T2))
 fpf-compatible(Id; x.Type; id-deq; ds2; fpf-join(id-deq; ds1; fpf-single(x; T1)))
 fpf-compatible(Id; x.Type; id-deq; ds1; fpf-join(id-deq; ds2; fpf-single(y; T2)))
 R-compat{i:l}
 R-compat(R-state-var(i; ds1; da; x; T1; ks1; tr1); R-state-var(i; ds2; da; y; T2; ks2; tr2)
 R-compat() 

latex

Definitions	x:A. B(x), decl-state(ds), P  Q, t  T, top, subtype(S; T), suptype(S; T), x. t(x), P  Q, P  Q, P  Q, prop{i:l}, x(s), ma-state(ds)
Lemmas	ma-state-subtype, fpf-sub-join-left2, fpf-sub weakening, ma-valtype wf, fpf-compatible-join-cap, fpf-cap-single1, subtype rel self, fpf-cap wf, top wf, decl-state wf, fpf-compatible wf, Id wf, id-deq wf, fpf-join wf, fpf-single wf, not wf, Knd wf, l member wf, fpf wf